(set-logic QF_BV)
(declare-fun _substvar_459_ () (_ BitVec 32))
(declare-fun _substvar_535_ () (_ BitVec 1))
(declare-fun _substvar_252_ () (_ BitVec 1))
(declare-fun _substvar_684_ () Bool)
(declare-fun _substvar_506_ () (_ BitVec 1))
(declare-fun _substvar_270_ () (_ BitVec 1))
(declare-fun _substvar_532_ () (_ BitVec 32))
(declare-fun _substvar_461_ () (_ BitVec 32))
(declare-fun _substvar_283_ () (_ BitVec 1))
(declare-fun _substvar_279_ () (_ BitVec 32))
(declare-fun _substvar_278_ () (_ BitVec 32))
(declare-fun _substvar_267_ () (_ BitVec 32))
(declare-fun _substvar_472_ () (_ BitVec 64))
(declare-fun _substvar_686_ () Bool)
(declare-fun _substvar_424_ () (_ BitVec 64))
(declare-fun _substvar_512_ () (_ BitVec 64))
(declare-fun _substvar_434_ () (_ BitVec 1))
(declare-fun _substvar_700_ () Bool)
(declare-fun _substvar_676_ () Bool)
(declare-fun _substvar_300_ () (_ BitVec 1))
(declare-fun _substvar_284_ () (_ BitVec 32))
(declare-fun _substvar_677_ () Bool)
(declare-fun _substvar_675_ () Bool)
(declare-fun _substvar_420_ () (_ BitVec 64))
(declare-fun _substvar_294_ () (_ BitVec 1))
(declare-fun _substvar_430_ () (_ BitVec 64))
(declare-fun _substvar_683_ () Bool)
(declare-fun _substvar_685_ () Bool)
(declare-fun _substvar_297_ () (_ BitVec 64))
(assert _substvar_700_)
(assert (= _substvar_420_ (bvshl _substvar_512_ (concat (_ bv0 56) ((_ extract 7 0) (_ bv2 64))))))
(assert (= _substvar_424_ (bvadd ((_ extract 63 0) (_ bv172 64)) _substvar_420_)))
(assert (= _substvar_430_ (bvadd _substvar_424_ (_ bv0 64))))
(assert (= (= _substvar_283_ (_ bv1 1)) (bvult (_ bv0 64) _substvar_430_)))
(assert (= _substvar_434_ _substvar_283_))
(assert (= false (= _substvar_267_ (_ bv0 32))))
(assert (= _substvar_459_ (ite (= _substvar_252_ (_ bv1 1)) _substvar_532_ (_ bv0 32))))
(assert (= _substvar_461_ (ite (= _substvar_434_ (_ bv1 1)) _substvar_459_ (_ bv0 32))))
(assert (= (= _substvar_300_ (_ bv1 1)) (= _substvar_461_ (_ bv0 32))))
(assert (= _substvar_506_ _substvar_300_))
(assert (= _substvar_279_ (ite (= _substvar_506_ (_ bv1 1)) _substvar_278_ (_ bv0 32))))
(assert (= (_ bv0 1) (bvand _substvar_294_ _substvar_506_)))
(assert (= _substvar_284_ (_ bv0 32)))
(assert _substvar_675_)
(assert _substvar_676_)
(assert _substvar_677_)
(assert (= _substvar_270_ (_ bv0 1)))
(assert (= (_ bv0 1) _substvar_535_))
(assert (= false (bvult _substvar_472_ _substvar_430_)))
(assert _substvar_683_)
(assert _substvar_684_)
(assert _substvar_685_)
(assert _substvar_686_)
(assert (= _substvar_297_ (_ bv0 64)))
(check-sat)
(exit)
